\newcommand{\metamodel}[1]{\mathit{MM}_{\!#1}}
\newcommand{\ocland}{\mathop{\,\text{and}\,}}
\newcommand{\oclimplies}{\mathop{\text{implies}}}
We apply the automated verification approach presented
in~\cite{Buettner2012ICFEM} to the GM-to-AUTOSAR transformation. In short, we
translate the ATL transformation $T$, its source metamodel $\metamodel{src}$,
and its target metamodel $\metamodel{tar}$ into a combined model, or
a \emph{transformation model}, consisting of $\metamodel{src}$ and
$\metamodel{tar}$ and additional model elements that represent the
transformation rules. Additionally, a set $\mathit{Sem}$ of OCL constraints is
generated for the combined model that characterizes the execution semantics of
the ATL rules. For declarative ATL rules without recursion, the constraints
describe the ATL semantics one-to-one, i.e., each valid instance of the
transformation model corresponds to an execution of the transformation and vice versa.
%TODO(FB): Mention abstraction and widening?

Using this representation we can check partial correctness of the transformation
with respect to properties specified as OCL constraints over the source and/or
the target model, by checking if there exists a counterexample within a
specific scope (i.e., maximum number of objects per class).
More specifically, for a set of transformation preconditions (or assumptions)
$\mathit{Pre}_1, \dots, \mathit{Pre}_n$ and a set of postconditions (or
assertions) $\mathit{Post}_1, \dots, \mathit{Post}_m$, we want to show that for
each instance $M$ of the transformation model,
\begin{equation}
\begin{split}
   \bigl( & \mathit{Sem}_1 \ocland \mathit{Sem}_2 \ocland \dots \ocland \mathit{Sem}_k \ocland \\
    & \mathit{Pre}_1 \ocland \mathit{Pre}_2 \ocland \dots \ocland \mathit{Pre}_n \bigr) \oclimplies  \\
    & \bigl(\mathit{Post}_1 \ocland \mathit{Post}_2 \ocland \dots \ocland \mathit{Post}_m \bigr)\\
\end{split}
\end{equation}
%
holds. This can be expressed equivalently as follows: For each postcondition
$\mathit{Post}_i$ ($1 \leq i \leq m$), the following formula must be
unsatisfiable (i.e., there is no model $M$ under which the formula is true):
\begin{equation}
 \mathit{Sem}_1 \ocland \dots \ocland \mathit{Sem}_k \ocland \mathit{Pre}_1
 \ocland \dots \ocland \mathit{Pre}_n \ocland \mathop{\text{not}}(\mathit{Post}_i)
 \label{eqn:unsatform}
\end{equation}
%
%FABIAN: Sorry, I know this construction is a bit messy ...
\begin{figure}[!b]%ht
  \centering
  \begin{minipage}[b]{0.33\linewidth}
    \subfigure[Source MM]{\includegraphics[scale=0.45]{imgs/ex-src-mm.pdf}}
    \subfigure[Target MM]{\ \includegraphics[scale=0.45]{imgs/ex-tar-mm.pdf}}\hspace*{-1ex}
  \end{minipage}%
  \begin{subfloat}
    \begin{minipage}[b]{0.63\linewidth}
      \begin{lstlisting}[language=ATL]
create OUT : Tar from IN : Src
rule R1 { from a : Src!A ( a.b->notEmpty() )
          to   c : Tar!C ( d <- a.b ) }
rule R2 { from a : Src!A ( a.b->isEmpty() )
          to   c : Tar!C ( d <- Set{d1} ), 
               d : TargetMM!D ( x <- 0 ) }
rule R3 { from b : Src!B  to d : Tar!D ( x <- b.x ) }
\end{lstlisting}
\vspace*{-0.5em}
  \end{minipage}
  \caption{ATL transformation}
\end{subfloat}\\
  \subfigure[b][Transformation model]{\includegraphics[scale=0.45]{imgs/ex-tm.pdf}}\hspace*{-1ex}
\begin{subfloat}
  \begin{minipage}[b]{0.67\linewidth}
    \begin{lstlisting}[language=ATL]
context a : A inv Sem_R1_match: a.b->notEmpty() implies 
  R1.allInstances()->one(r1|r1.a = a)
context R1 inv Sem_R1_cond: self.a.b->notEmpty()
context R1 inv Sem_R1_bind_c: 
  self.d->forAll(d | self.a.b->exists(b | b.r2 = d) and
  self.a.b->forAll(b | self.d->exists(b | b.r2 = d)
context R3 inv Sem_R3_bind_d: self.d.x = self.b.x
context C inv Sem_C_create: 
  self.r1->size() + self.r2->size() = 1
\end{lstlisting}
\vspace*{-0.5em}
\end{minipage}
\caption{OCL constraints for ATL semantics (excerpt)}
\end{subfloat}\\
\hspace*{-3ex}
\begin{subfloat}
  \begin{minipage}[b]{0.51\linewidth}
\begin{lstlisting}[language=ATL]
context A inv Pre1: self.b.x->sum() >= 0
context A inv Pre2: self.b->size() >= 1
\end{lstlisting}
\end{minipage}
\caption{Preconditions}
\end{subfloat}\hspace*{-3ex}
\begin{subfloat}
  \begin{minipage}[b]{0.51\linewidth}
\begin{lstlisting}[language=ATL]
context C inv Post1: self.d->size() >= 1
context C inv Post2: self.b.x->sum() >= 0
\end{lstlisting}
\end{minipage}
\caption{Postconditions}
\end{subfloat}
\caption{Transformation model example}
\label{fig:tmexample}
\end{figure}

\vspace*{-0.3cm}
Fig.~\ref{fig:tmexample} illustrates this using a simple example. In the upper
part we have an ATL transformation (c) over the shown source and target
metamodels (a) and (b). The transformation copies the A-B structure to the C-D
structure, but creates an additional D object when copying an `empty' A object.
The middle part shows the transformation model of this transformation. In the
class diagram (d), each of the three rules is translated into a trace class and
connected to the source and target classes according to the \emph{from} and
\emph{to} patterns of the rule. The OCL constraints (e) capture the execution
semantics of the transformation such as the matching of rule R1, the binding of
primitive and object-typed properties, and the controlled creation of target
objects. Some pre-/post- conditions are shown in (f) and (g), respectively.


To verify that, for example, postcondition $\mathit{Post_i}$ is implied by the
transformation (given the preconditions), we have to check that \begin{changebar}Eq.~(\ref{eqn:unsatform})\end{changebar} is unsatisfiable.
% \begin{equation}
%  \mathit{Pre_1} \ocland \mathit{Pre_2} \ocland \langle\text{sem
% constraints}\rangle \ocland \mathop{not}(\mathit{Post_1})
% \label{eqn:exampleToVerif} 
% \end{equation}
% has no instances or counterexamples.
\begin{changebar}This can \end{changebar}be tested using metamodel satisfiability checkers, or
\emph{model finders}, such as the USE
Validator~\cite{Kuhlmann2011} which is publicly \begin{changebar}available~\cite{USE}.\end{changebar}
The USE Validator translates the UML model and the OCL constraints into a relational
logic formula and employs the SAT-based solver Kodkod~\cite{Torlak2007Kodkod} to
check \begin{changebar}the unsatisfiability of Eq.~(\ref{eqn:unsatform}) for each of the
post-conditions $\mathit{Post_i}$ within a given scope.\end{changebar}
%\footnote{In the USE
%validator, the scope limits the search space by putting an upper bound on the
%number of times a class can be instantiated.}.
%the generated formula can satisfy Equation \ref{eqn:exampleToVerif} within
% given scopes (i.e., number of objects per class).
Thus, we have four different representations of the problem space, (i) ATL +
OCL, (ii) OCL, (iii) relational logic, and (iv) propositional logic (for the
SAT solver).

We have implemented the whole chain as an verification prototype
(Fig.~\ref{fig:toolchain}). We have \begin{changebar}implemented\end{changebar} the ATL-to-OCL
transformation~\cite{Buettner2012ICFEM} as a higher-order ATL
transformation~\cite{Tisi2009HOT}, i.e., a transformation from Ecore and ATL
metamodels to Ecore metamodels (where the Ecore model can contain OCL
constraints as annotations).
\begin{changebar}
 Our implementation automatically generates the \emph{Sem} constraints from the ATL transformation as well as \emph{Pre} and \emph{Post} constraints from the structural constraints in the source and target metamodels (further constraints to be verified can be added manually).    
\end{changebar}
Since the USE validator has a proprietary \begin{changebar}metamodel syntax\end{changebar}, we have created a converter from Ecore \begin{changebar}to
generate a \emph{USE specification}.\end{changebar} We also generate a default search space
configuration, which is a file specifying the scopes and ranges for the
attribute values. In the search configuration, we can disable or negate
individual invariants or constraints.
\begin{figure}[h!]
  \centering
%  \subfigure[Problem representations]{\includegraphics[scale=0.45]
%  {imgs/problemrepresentations.pdf}\label{fig:problemrepresentations}}\quad\quad
%  \subfigure[Tool chain]{
  \includegraphics[scale=0.38] {imgs/toolchain.pdf}\\[-2ex]
  \caption{The tool chain used to perform the transformation verification.}
  \label{fig:toolchain}
\end{figure}

{\bf{\emph{Steps to verify a postcondition using the prototype:}}} To \begin{changebar}check Eq.~(\ref{eqn:unsatform})\end{changebar} for a postcondition, we have
to negate the respective postcondition and disable all other postconditions in
the generated \emph{search configuration} (Fig.~\ref{fig:toolchain}) and then
run USE.
% We then run USE on the updated \emph{search configuration} to verify the
% postcndition. 
If USE reports `unsat', this implies that there is no input model
in the search space for which the transformation can produce an output model
that violates the postcondition. If there exists a counterexample, USE provides
the object diagram of the counterexample which can be analyzed using many
browsing features of the tool. Although the implementation is a prototype, it is
not specific to the GM-to-AUTOSAR transformation.
%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "main"
%%% End: 